package com.googlecode.kipler.transformations;

import java.util.Set;

import com.googlecode.kipler.container.dl.ABox;
import com.googlecode.kipler.container.dl.SHOIQIndividual;
import com.googlecode.kipler.container.dl.World;
import com.googlecode.kipler.container.dl.WorldConstraintSystem;
import com.googlecode.kipler.satisfiability.reasoner.Reasoner;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.syntax.concept.Nominal;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;
import com.googlecode.kipler.syntax.formula.Formula;


/**
 * 
 * @author İnanç Seylan
 *
 */
public class SHOIQPreprocessingStrategy implements
		SyntacticalProcessingStrategy {
	private Reasoner reasoner;

	public SHOIQPreprocessingStrategy(Reasoner reasoner) {
		this.reasoner = reasoner;
	}

	public WorldConstraintSystem process(Set<Formula> formulaSet) {
		WorldConstraintSystem result = reasoner.getProfile().getWcsFactory()
				.createWcs();
		World world = result.createWorld();
		for (Formula formula : formulaSet) {
			formula = formula.copy();
			FormulaSimplificationVisitor simpleVisitor = new FormulaSimplificationVisitor();
			formula.accept(simpleVisitor);
			formula = simpleVisitor.getNormalForm();
			world.addSilent(formula);
			addABoxIndividualsAsNominals(world.getABox(), formula);
		}
		return result;
	}

	private void addABoxIndividualsAsNominals(ABox abox, Formula formula) {
		IndividualCollectionFromFormulaVisitor visitor = new IndividualCollectionFromFormulaVisitor();
		formula.accept(visitor);
		try {
			for (String indvName : visitor.getOldIndividualSet()) {
				abox.add(new ConceptAssertion(new Nominal(indvName), indvName));
				SHOIQIndividual indv = (SHOIQIndividual) abox
						.getIndividual(indvName);
				indv.setLevel(0);
			}
		} catch (UnsatisfiableException e) {
			// will never reach here because none of the above assertions is
			// unsatisfiable
		}
	}
}
